package var.satisfiability;

import java.util.ArrayList;
import java.util.Collections;
import java.util.Iterator;
import java.util.List;
import java.util.Set;
import java.util.Stack;

import tr.edu.ege.kipler.satisfiability.BranchingException;
import tr.edu.ege.kipler.satisfiability.ReasonerException;
import tr.edu.ege.kipler.satisfiability.Reasoner;
import tr.edu.ege.kipler.satisfiability.UnsatisfiableException;
import tr.edu.ege.kipler.satisfiability.completion.rules.CompletionRule;
import tr.edu.ege.kipler.satisfiability.completion.rules.EmptyDomainRule;
import tr.edu.ege.kipler.satisfiability.completion.rules.RuleLogger;
import tr.edu.ege.kipler.satisfiability.completion.rules.dl.ABoxRule;
import tr.edu.ege.kipler.satisfiability.completion.rules.dl.AllValuesRule;
import tr.edu.ege.kipler.satisfiability.completion.rules.dl.IntersectionRule;
import tr.edu.ege.kipler.satisfiability.completion.rules.dl.NegatedConceptDefinitionRule;
import tr.edu.ege.kipler.satisfiability.completion.rules.dl.PositiveConceptDefinitionRule;
import tr.edu.ege.kipler.satisfiability.completion.rules.dl.SomeValuesRule;
import tr.edu.ege.kipler.satisfiability.completion.rules.dl.UnionRule;
import tr.edu.ege.kipler.satisfiability.completion.rules.formula.BoxFormulaRule;
import tr.edu.ege.kipler.satisfiability.completion.rules.formula.ConjunctionRule;
import tr.edu.ege.kipler.satisfiability.completion.rules.formula.DiamondFormulaRule;
import tr.edu.ege.kipler.satisfiability.completion.rules.formula.DisjunctionRule;
import tr.edu.ege.kipler.satisfiability.container.Individual;
import tr.edu.ege.kipler.satisfiability.container.World;
import tr.edu.ege.kipler.satisfiability.container.WorldConstraintSystem;
import tr.edu.ege.kipler.satisfiability.container.operational.IndividualNameComparator;
import tr.edu.ege.kipler.satisfiability.container.operational.IndividualNameManager;
import tr.edu.ege.kipler.satisfiability.syntactical.FormulaSimplificationVisitor;
import tr.edu.ege.kipler.satisfiability.syntactical.IndividualCollectionFromFormulaVisitor;
import tr.edu.ege.kipler.satisfiability.syntactical.TopConsistenceNormalFormVisitor;
import tr.edu.ege.kipler.syntax.WorldElement;
import tr.edu.ege.kipler.syntax.atomicformula.ConceptAssertion;
import tr.edu.ege.kipler.syntax.concept.ConceptName;
import var.satisfiability.rules.BoxConceptRule;
import var.satisfiability.rules.ConstantDomainRule;
import var.satisfiability.rules.DiamondConceptRule;
import var.syntax.BeliefOperator;


/**
 * This is the public interface to the tableau algorithm. It supports two main
 * operations which are satisfiability checking of a set of formulae, and
 * determining whether a given formula is logically inferred from a set of
 * formulae.
 * 
 * @author Inanc Seylan
 * 
 */
public class KALCReasoner implements Reasoner {
	private List<ABoxRule> aboxRuleList = new ArrayList<ABoxRule>();

	private List<CompletionRule> globalRuleList = new ArrayList<CompletionRule>();

	private WorldConstraintSystem currentWcs;

	/**
	 * This stack is used to simulate the tree characteristic of the tableu
	 * algorithm. Each application of the disjunction rule generates a new world
	 * constraint system. We have to consider each of these world constraint
	 * systems until one is found that is complete and satisfiable. This stack
	 * allows us to visit these world constraint systems as if we're traversing
	 * a tree.
	 */
	private Stack<WorldConstraintSystem> branchingStack = new Stack<WorldConstraintSystem>();

	/**
	 * This field is used to store the initial set of formulae.
	 */
	private World initialWorld = new World();

	private int lastWcsId;

	/**
	 * Default constructor. It creates the instances of the tableau rules and
	 * adds them to {@link #aboxRuleList}. The order which they are added to
	 * the rule list is important because it determines their order of
	 * application in a world.
	 * 
	 */
	public KALCReasoner() {
		aboxRuleList.add(new PositiveConceptDefinitionRule());
		aboxRuleList.add(new IntersectionRule());
		aboxRuleList.add(new UnionRule(this));
		aboxRuleList.add(new AllValuesRule());
		aboxRuleList.add(new SomeValuesRule());
		aboxRuleList.add(new DiamondConceptRule(BeliefOperator
				.diamondBelief("")));
		aboxRuleList.add(new BoxConceptRule(BeliefOperator.boxBelief("")));

		globalRuleList.add(new ConjunctionRule());
		globalRuleList.add(new DisjunctionRule(this));
		globalRuleList.add(new DiamondFormulaRule(BeliefOperator
				.diamondBelief("")));
		globalRuleList.add(new BoxFormulaRule(BeliefOperator.boxBelief("")));
	}

	/**
	 * @return the last world constraint system that the prover modified. If
	 *         there aren't any conjunctive formulae in worlds generated, then
	 *         the return constraint system is actually the initial world
	 *         constraint system. Otherwise it's the last of the modified
	 *         constraints systems.
	 */
	public WorldConstraintSystem getCurrentWcs() {
		return currentWcs;
	}

	/**
	 * This method executes all the reduction laws that this logic has on the
	 * given formula. These rules are explained in {@link KD45NormalFormVisitor},
	 * {@link BelievedIntentionNormalFormVisitor}, and
	 * {@link NeighborhoodToMultiModalVisitor}.
	 * 
	 * @param formula
	 *            The formula to be simplified
	 * @return the simplified form of the input formula.
	 */
	private WorldElement generateNormalForm(WorldElement formula) {
		try {
			formula = formula.clone();
			TopConsistenceNormalFormVisitor topVisitor = new TopConsistenceNormalFormVisitor();
			formula.accept(topVisitor);
			formula = topVisitor.getNormalForm();
			FormulaSimplificationVisitor simpleVisitor = new FormulaSimplificationVisitor();
			formula.accept(simpleVisitor);
			formula = simpleVisitor.getNormalForm();
		} catch (CloneNotSupportedException e) {
			// TODO Auto-generated catch block
			e.printStackTrace();
		}
		return formula;
	}

	private void addOldIndividualsToABox(WorldElement formula) {
		IndividualCollectionFromFormulaVisitor visitor = new IndividualCollectionFromFormulaVisitor();
		formula.accept(visitor);
		try {
			for (String indv : visitor.getOldIndividualSet()) {
				initialWorld.add(new ConceptAssertion(ConceptName.topConcept(),
						indv));
			}
		} catch (UnsatisfiableException e) {
			// will never reach here because none of the above assertions is
			// unsatisfiable
		}
	}

	/**
	 * Adds the given formula to the initial set of formulae after applying the
	 * reduction laws to it.
	 * 
	 * @param formula
	 *            The formula to be added.
	 */
	public void addFormula(WorldElement formula) {
		try {
			WorldElement normalForm = generateNormalForm(formula);
			addOldIndividualsToABox(normalForm);
			initialWorld.add(normalForm);
		} catch (UnsatisfiableException e) {
		}
	}

	public void addFormulasOfWorld(World world) {
		for (WorldElement formula : world.getFormulas()) {
			addFormula(formula);
		}
	}

	/**
	 * Applies the rules of tableau to all worlds in a world constraint system.
	 * The case of the disjunction rule is treated specially. If the disjunction
	 * rule is applied to a wcs, this method ends for that wcs.
	 * 
	 */
	private void applyRules() throws ReasonerException {
		boolean constDomainApplied;
		int initialSize, finalSize;
		do {
			Set<World> worlds = getCurrentWcs().getAllWorlds();
			initialSize = worlds.size();
			for (World world : worlds) {
				expandWorldWithGlobalRules(world);
				expandWorldWithLocalRules(world);
			}
			finalSize = getCurrentWcs().getAllWorlds().size();
			constDomainApplied = false;
			CompletionRule compRule = new ConstantDomainRule(getCurrentWcs(),
					null);
			compRule.apply();
			constDomainApplied = compRule.isApplied();
		} while (constDomainApplied || finalSize > initialSize);
	}

	/**
	 * @param disjunctionApplied
	 * @param world
	 * @return
	 */
	private void expandWorldWithLocalRules(World world) throws ReasonerException {
		boolean ruleApplied = false;
		CompletionRule compRule = new NegatedConceptDefinitionRule(
				getCurrentWcs(), world);
		compRule.apply();
		compRule = new EmptyDomainRule(getCurrentWcs(), world);
		compRule.apply();
		do {
			List<Individual> result = new ArrayList<Individual>();
			for (Iterator<Individual> i = world.getABox().individualIterator(); i
					.hasNext();) {
				result.add(i.next());
			}
			Collections.sort(result, new IndividualNameComparator());
			ruleApplied = false;
			for (Individual individual : result) {
				for (ABoxRule rule : aboxRuleList) {
					rule.setWcs(getCurrentWcs());
					rule.setWorld(world);
					rule.setIndividual(individual);
					rule.apply();
					ruleApplied = ruleApplied || rule.isApplied();
				}
			}
		} while (ruleApplied);
	}

	private void expandWorldWithGlobalRules(World world) throws ReasonerException {
		for (CompletionRule rule : globalRuleList) {
			rule.setWcs(getCurrentWcs());
			rule.setWorld(world);
			rule.apply();
		}
	}

	/**
	 * This method pushes two world constraint systems into the stack. The only
	 * difference between these two world constraint systems is a world. In the
	 * first wcs, this world has the left operand of a disjunction and in the
	 * second wcs, this world has the right operand.
	 * 
	 * @param leftNode
	 *            The wcs with the world containing the left operand of a
	 *            disjunction.
	 * @param rightNode
	 *            The wcs with the world containing the right operand of a
	 *            disjunction.
	 */
	public void addBranch(WorldConstraintSystem wcs) {
		if (wcs != null) {
			branchingStack.push(wcs);
			wcs.setId(++lastWcsId);
		}
	}

	/**
	 * @return true if the initial set of formulae supplied to the prover is
	 *         satisfiable.
	 * @throws Exception
	 */
	public boolean isSatisfiable() throws Exception {
		World initialWorldClone = initialWorld.copy();
		return isSatisfiable(initialWorldClone);
	}

	/**
	 * This method checks if the given formula is a logical consequence of the
	 * initial set of formulae. The algorithm is actually the satisfiability
	 * checking of the set of initial formulae supplied with the negation of the
	 * input formula.
	 * 
	 * @param formula
	 *            The formula to be checked if it's logically inferred.
	 * @return true if the given formula is logically inferred from the initial
	 *         set of formulae supplied to the prover.
	 * @throws Exception
	 */
	public boolean isLogicalConsequence(WorldElement formula) throws Exception {
		WorldElement normalForm = formula.clone();
		normalForm.toggleNegated();
		normalForm = generateNormalForm(normalForm);
		World initialWorldClone = initialWorld.copy();
		initialWorldClone.add(normalForm);
		return !isSatisfiable(initialWorldClone);
	}

	private void initProver(World initialWorld) {
		lastWcsId = 0;
		IndividualNameManager.getInstance().reset();
		currentWcs = new WorldConstraintSystem();
		currentWcs.setId(lastWcsId);
		currentWcs.nameWorld(initialWorld);
		branchingStack.clear();
		branchingStack.add(currentWcs);
	}

	/**
	 * This method executes the satisfiability checking algorithm for the
	 * supplied initial set of formulae.
	 * 
	 * @param initialWorld
	 *            The world in which the initial set of formulae reside.
	 * @return true if the initial set of formulae is satisfiable.
	 * @throws Exception
	 */
	private boolean isSatisfiable(World initialWorld) {
		initProver(initialWorld);
		// if the initial world constraint system is unsatisfiable already
		if (!initialWorld.isSatisfiable()) {
			return false;
		}
		boolean result = false;
		while (!branchingStack.empty() && !result) {
			currentWcs = branchingStack.pop();
			try {
				applyRules();
				result = true;
			} catch (BranchingException e) {
				result = false; // next iteration
			} catch (UnsatisfiableException e) {
				result = false; // next iteration
				RuleLogger.getInstance()
						.info(
								"WCS " + getCurrentWcs().getId()
										+ " is unsatisfiable.");
			} catch (ReasonerException e) {
				// will never come here
			}
		}
		return result;
	}

}
